\documentclass{article}
\usepackage{url}
\usepackage{manfnt}
\usepackage{fullpage}
\usepackage{proof}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{xcolor}
\usepackage{mathrsfs}
\usepackage{amsmath, amsthm}

\newcommand{\fomega}[0]{$\mathbf{F}_{\omega}\ $}
\newcommand{\frank}[1]{\textcolor{blue}{\textbf{[#1 --Frank]}}}
% My own macros
\newcommand{\m}[2]{ \{\mu_{#1}\}_{#1 \in #2}} 
\newcommand{\M}[3]{\{#1_i \mapsto #2_i\}_{i \in #3}} 
\newcommand{\bred}[0]{\to_{\beta}} 
\newcommand{\rat}[0]{\rightarrowtail} 
\newcommand{\polym}[1]{\rightarrowtail_{#1}} 
\newcommand{\tyred}[0]{\rightarrowtail_{\tau}} 
\newtheorem{prop}{Proposition}
\newtheorem{definition}{Definition}
\newtheorem{corollary}{Corollary}
\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}

\begin{document}
%\pagestyle{empty}
\title{Type Preservation for Curry Style $\mathbf{F}_{\omega}$}
\author{Peng Fu \\
Computer Science, The University of Iowa}
\date{last edited: \today}


\maketitle
\thispagestyle{empty}
 
\section{System \fomega}

\begin{definition}[Syntax]

\

\noindent \textit{Terms} $t \ :: = \ x \ | \ \lambda x.t \ | \ t t'$

\noindent \textit{Types} $T \ ::= \ X \ | \ \Delta X:\kappa.T \ | \ T_1 \to T_2 \ | \ \lambda X.T \ | \ T_1 T_2$

\noindent \textit{Kinds} $\kappa \ ::= \ * \ | \ \kappa' \to \kappa$. 

\noindent \textit{Context} $\Gamma \ :: = \ \cdot \ | \ \Gamma, x:T \ |  \ \Gamma, X:\kappa $ 

%% \noindent Let $\tilde{\mu}_c$ be the following recursive defintions:

%% \noindent $(\mathsf{Nat}:* ) \mapsto \iota x. \forall C: (\xi x:\mathsf{Nat}. *).  (\Pi n : \mathsf{Nat}. (C\ n) \to (C\ (\mathsf{S}\ n))) \to (C\ 0) \to (C\ x)$

%% \noindent $(\mathsf{S}: \mathsf{Nat} \to \mathsf{Nat} )\mapsto \lambda n. \lambda s.\lambda z. s \ [n]\ (n\ s\ z)$

%% \noindent $(0:\mathsf{Nat})  \mapsto \lambda s. \lambda z.z$


\end{definition} 

\noindent \textbf{Note}: I use $\Delta X:\kappa.T$ to represent polymorphic functional types. I 
would have chose $\Pi$ construct, but that will conflict Martin L\"of's index functional types.
So I choose Reynold's notation. The reason that I do not use $\forall$ is that it is a logical
symbol, and it will blur the point of functional interpretation, namely,
logic can be interpreted as part of the functional theory, but not the other way around. 

\begin{definition}[Well-formed Context]
\

\begin{tabular}{ll}
\infer{ \cdot \vdash \mathsf{wf}}{}

&

\infer{ \Gamma, x:T \vdash \mathsf{wf}}{\Gamma \vdash \mathsf{wf} & \Gamma \vdash T:*}

\end{tabular}

\end{definition}


\begin{definition}[Kinding]
\


\begin{tabular}{lll}
\infer[\textit{KVar}]{\Gamma \vdash X:\kappa}{(X:\kappa) \in \Gamma}

&

\infer[\textit{Func}]{\Gamma \vdash T_1 \to T_2 : *}{ \Gamma \vdash T_1 : * &
\Gamma \vdash T_2 : *}

&

\infer[\textit{Poly}]{\Gamma \vdash \Delta X:\kappa. T : *}{ \Gamma, X:\kappa \vdash T : *}

\\
\\
\infer[\textit{TAbs}]{\Gamma \vdash \lambda X.T: \kappa \to \kappa'}{\Gamma, X:\kappa \vdash T : \kappa' }

&

\infer[\textit{TApp}]{\Gamma \vdash S T: \kappa}{\Gamma \vdash S: \kappa' \to \kappa & 
\Gamma \vdash T:\kappa'}


\\

\end{tabular}

\end{definition}

\begin{definition}[Typing Rules]
\


\begin{tabular}{lll}
    
\infer[\textit{Var}]{\Gamma \vdash x:T}{(x:T) \in \Gamma}

&

\infer[\textit{Conv}]{\Gamma \vdash t : T_2}{\Gamma \vdash t:
T_1 & \Gamma \vdash T_1 \simeq_{\tau} T_2 & \Gamma \vdash T_2:*}

&
\infer[\textit{Func}]{\Gamma \vdash \lambda x.t :T_1 \to T_2}
{\Gamma, x:T_1 \vdash t: T_2 & \Gamma \vdash T_1:*}

\\
\\
\infer[\textit{App}]{\Gamma \vdash t t':T_2}{\Gamma
\vdash t:T_1 \to T_2 & \Gamma \vdash t': T_1}

&

\infer[\textit{Gen}]{\Gamma \vdash t :\Delta X:\kappa.T}
{\Gamma, X:\kappa \vdash t: T}

&
\infer[\textit{Inst}]{\Gamma \vdash t:[T'/X]T}{\Gamma \vdash t: \Delta X:\kappa.T 
& \Gamma \vdash T': \kappa}

\end{tabular}

\end{definition}

\noindent \textbf{Note}: $\simeq_{\tau}$ is the reflexive transitive and symmetry closure of $\tyred$.
\begin{definition}[Type Reductions]
\

\begin{tabular}{llll}
  \infer{(\lambda X.T)T' \tyred [T'/X]T }{}

&

  \infer{T T' \tyred T T'' }{ T' \tyred T''}

&
  \infer{T T' \tyred T'' T' }{ T \tyred T''}

&
  \infer{T \to T' \tyred T\to T'' }{ T' \tyred T''}

\\
\\

  \infer{T \to T' \tyred T''\to T' }{ T \tyred T''}

&
  \infer{\Delta X:\kappa. T \tyred \Delta X:\kappa. T' }{ T \tyred T'}

&
  \infer{ \lambda X. T \tyred \lambda X. T' }{ T \tyred T'}

\end{tabular}
\end{definition}

\begin{definition}[Term Reductions]
\

\begin{tabular}{llll}
  \infer{(\lambda x.t)t' \bred [t'/x]t }{}

&

  \infer{t t' \bred t t'' }{ t' \bred t''}

&
  \infer{t t' \bred t'' t' }{ t \bred t''}

&

  \infer{ \lambda x. t \bred \lambda x. t' }{ t \bred t'}

\end{tabular}
  
\end{definition}


\section{Morph Analysis}

\begin{definition}[Morphing]
\

  \begin{itemize}
  \item $ T_1 \polym{i} T_2$ if $T_1 \equiv \Delta X:\kappa.T$ and $T_2 \equiv [T'/X]T$ for some
$T'$.
  \item $T_1 \polym{g} T_2$ if  $T_2 \equiv \Delta X:\kappa.T_1$ for some $X, \kappa$.
  \end{itemize}
\end{definition}

\noindent Let ${\polym{i,g}^*}$ be the reflexive and transitive closure of $\polym{i} \cup \polym{g}$. Let $\overline{\Gamma} = \Gamma, X_1:\kappa_1,..., X_n:\kappa_n$ for some $\{X_i:\kappa_i\}_{i\in N}$. 


\begin{definition}
\

  \begin{tabular}{lllll}
  $o(\Delta X:\kappa.T) := o(T)$
&
  $o(X) := X$

&

 $o(T_1 \to T_2) := T_1 \to T_2$

&
$o(\lambda X.T) := \lambda X.T$

&

$o(T_1 T_2) := T_1 T_2$
  \end{tabular}
\end{definition}

\begin{lemma}
\label{sub}
  $o([T/X]T') \equiv [T''/X]o(T')$ for some $T''$. 
\end{lemma}
\begin{proof}
  By induction on structure of $T'$. 
\end{proof}

\noindent \textbf{Note}: We do not have: if $T =_{\beta}T'$, then $o(T) =_{\beta}o(T')$. Due to 
the fact that we do not have $o([T_1/X]T_2) \equiv [o(T_1)/X]o(T_2)$.

\begin{lemma}
\label{elim}
  If $T {\polym{i,g}^*} T'$, then there exist a type substitution $\sigma$ such that $\sigma o(T) \equiv o(T')$. 
\end{lemma}
\begin{proof}
  It suffices to consider $T {\polym{i,g}} T'$.
If $T' \equiv \Delta X:\kappa .T$, then $o(T') \equiv o(T)$.
If $T \equiv \Delta X:\kappa .T_1$ and $T' \equiv [T''/X]T_1$, then $o(T) \equiv o(T_1)$. By lemma \ref{sub} above, we know $o(T') \equiv o([T''/X]T_1) \equiv [T_2/X]o(T_1)$ for some $T_2$. 
\end{proof}

\begin{lemma}
  If $T_1 \to T_2 {\polym{i,g}^*} T_1' \to T_2'$, then there exist a type substitution $\sigma$
such that $\sigma(T_1 \to T_2) \equiv T_1' \to T_2'$.
\end{lemma}

\begin{proof}
  By lemma \ref{elim} above.
\end{proof}

\noindent Let $\rat_{i,g,\tau}^*$ denotes $(\polym{i,g}^* \cup \simeq_{\tau})^*$.
\begin{theorem}[Compatibility]
\label{comp}
  If $T_1 \to T_2  \rat_{i,g,\tau}^* T_1' \to T_2'$, then there exist a type substitution $\sigma$ such that $\sigma(T_1 \to T_2) \simeq_{\tau} T_1' \to T_2'$.
\end{theorem}

\section{Type Preservation}

\begin{lemma}
  Let $T_1 {\rat_{i,g,\tau}^*} T_2$. Then $\Gamma \vdash t:T_1$ implies $\Gamma_1 \vdash t:T_2$, where $\Gamma = \overline{\Gamma}_1$. 
\end{lemma}

\begin{lemma}[Inversion I]
If $\Gamma \vdash x:T$, then exist $\Gamma_1, T_1$ such that $T_1 {\polym{i,g,\tau}^*} T$
and $(x:T_1) \in \Gamma_1$ and $\Gamma_1 = \overline{\Gamma}$. 
\end{lemma}

\begin{lemma}[Inversion II]
If $\Gamma \vdash t_1 t_2:T$, then exist $\Gamma_1, T_1, T_2$ such that $\Gamma_1 \vdash t_1:T_1 \to T_2$ and $\Gamma_1 \vdash t_2:T_1$ and $ T_2 {\polym{i,g, \tau}^*} T$ with $\Gamma_1 = \overline{\Gamma}$. 
\end{lemma}

\begin{lemma}[Inversion III]
If $\Gamma \vdash \lambda x.t:T$, then exist $\Gamma_1, T_1, T_2$ such that $\Gamma_1, x:T_1 \vdash t:T_2$ and $T_1 \to T_2 {\polym{i,g, \tau}^*} T$ with $\Gamma_1 = \overline{\Gamma}$. 
\end{lemma}

\begin{lemma}[Substitution]
\label{subst}
\

  \begin{enumerate}
  \item   If $\Gamma \vdash t:T$, then for any type substitution $\sigma$, $\sigma \Gamma \vdash t: \sigma T$.
\item If $\Gamma, x:T \vdash t:T'$ and $\Gamma \vdash t':T$, then $\Gamma \vdash [t'/x]t:T'$.
  \end{enumerate}

\end{lemma}

\begin{proof}
  By induction on derivation.
\end{proof}
\begin{theorem}[Type Preservation]
  If $\Gamma \vdash t:T$ and $t \to_{\beta} t'$, then $\Gamma \vdash t':T$.
\end{theorem}
\begin{proof}
  By induction on derivation of $\Gamma \vdash t:T$. We only show one interesting 
case here:

\

\infer[\textit{App}]{\Gamma \vdash t t':T_2}{\Gamma
\vdash t:T_1 \to T_2 & \Gamma \vdash t': T_1}

\

\noindent Suppose $(\lambda x.t_1) t_2 \to_{\beta} [t_2/x]t_1$. We know that
$\Gamma \vdash \lambda x.t_1 : T_1 \to T_2$ and $\Gamma \vdash t_2:T_1$. By
inversion on $\Gamma \vdash \lambda x.t_1 : T_1 \to T_2$, we know that 
there exist $\Gamma_1, T_1', T_2'$ such that $\Gamma_1, x:T_1' \vdash t_1:T_2'$
and $T_1'\to T_2' {\polym{i,g, \tau}^*} T_1 \to T_2$ with $\Gamma_1 = \overline{\Gamma}$.
By theorem \ref{comp}, we have $\sigma(T_1'\to T_2') \simeq_{\tau} T_1 \to T_2$. By Church-Rosser
of $\simeq_{\tau}$, we have $\sigma T_1' \simeq_{\tau} T_1$ and $\sigma T_2' \simeq_{\tau} T_2$. 
So by (1) of lemma \ref{subst}, we have $\Gamma_1, x:\sigma T_1' \vdash t_1: \sigma T_2'$. Thus 
$\Gamma, x:T_1 \vdash t_1:T_2$. Since $\Gamma \vdash t_2:T_1$. By (2) of lemma \ref{subst}, $\Gamma \vdash [t_2/x]t_1: T_2$. 
\end{proof}


\end{document}
